A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  ((I|p)(e) = I(e)  A) 

latex

Definitions	P  Q, x:A. B(x), x. t(x), E, f(a), x(s), b, Dec(P), x:AB(x), Type, , Top, left + right, ES, X(e), (I|p), e  X, AbsInterface(A)
Lemmas	do-apply-p-restrict